es:event_system{i:l}, L:(Id List), del:rationals.
fischer{x:ut2, try:ut2, taken:ut2, contending:ut2, free:ut2, mine:ut2, wanted:ut2, z:ut2}
fischer(es; L)
 fischer-delay{i:l,
 fischer-delay{x:ut2,
 fischer-delay{try:ut2,
 fischer-delay{taken:ut2,
 fischer-delay{contending:ut2,
 fischer-delay{free:ut2,
 fischer-delay{mine:ut2,
 fischer-delay{wanted:ut2,
 fischer-delay{z:ut2}
 fischer-delay(es; del; L)
 (e:es-E(es). 
 (loc(e)  L)
  @e(mkid{x:ut2}mkid{free:ut2})
  (e':es-E(es). 
  es-locl(es; e; e')
   qless(es-time(es; e'); (es-time(es; e) + del))
   (es-when(es; mkid{x:ut2}; e') = mkid{free:ut2}  Id))) 

latex

Definitions

es-dtype(es; i; x; T), if b then t else f fi , ff, eq_atom{$n:n}(x; y), atom2-deq, id-deq, t.1, eqof(d), P  Q, eq_id(a; b), P  Q, A c B, P  Q, b, A, @e(xv), True, T, guard(T), sq_type(T), x. t(x), P  Q, prop{i:l}, t  T, es-locl(es; e; e'), mkid{$x:ut2}, P  Q, Id, x:A. B(x), False, fischer-delay, fischer, x(s), wellfounded{i:l}(A; x,y.R(x;y)), !hyp_hide(x)  {FDLNOr12445}

Lemmas

qless irreflexivity, qless transitivity 2 qorder, es-vartype wf, es-isconst wf, id-deq wf, unchanged-for-change-to, false wf, assert-eq-id, eq id wf, assert wf, not functionality wrt iff, qless transitivity 1 qorder, es-causle weakening, es-causl weakening, es-pred-causl, es-causle-time, es-pred-locl, es-pred wf, es-after wf, true wf, squash wf, es-after-pred2, es-locl-iff, es-loc-pred, Id sq, es-locl-wellfnd, qadd wf, es-time wf, qless wf, es-when wf, es-causl wf, event system wf, Id wf, rationals wf, fischer wf, fischer-delay wf, es-E wf, es-loc wf, l member wf, es-change-to wf